
%%%%%%%%%%%%%%%%%%%%%%% file typeinst.tex %%%%%%%%%%%%%%%%%%%%%%%%%
%
% This is the LaTeX source for the instructions to authors using
% the LaTeX document class 'llncs.cls' for contributions to
% the Lecture Notes in Computer Sciences series.
% http://www.springer.com/lncs       Springer Heidelberg 2006/05/04
%
% It may be used as a template for your own input - copy it
% to a new file with a new name and use it as the basis
% for your article.
%
% NB: the document class 'llncs' has its own and detailed documentation, see
% ftp://ftp.springer.de/data/pubftp/pub/tex/latex/llncs/latex2e/llncsdoc.pdf
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\documentclass[runningheads]{llncs}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}

\usepackage{url}
\urldef{\mailsa}\path|{alfred.hofmann,ursula.barth,ingrid.beyer,natalie.brecht,|
\urldef{\mailsb}\path|christine.guenther,frank.holzwarth,piamaria.karbach,|
\urldef{\mailsc}\path|anna.kramer,erika.siebert-cole,lncs}@springer.com|
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{Formal Specification and Verification of a Narrow Bandwidth Protocol in PVS}

% a short form should be given in case it is too long for the running head
\titlerunning{Formal Specification and Verification of a Narrow Bandwidth Protocol}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{Hai Wan\inst{1,} \inst{2}, Ming Gu \inst{2} and Xiaoyu Song \inst{3}}
%
\authorrunning{Hai Wan, Ming Gu, Xiaoyu Song}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{CST Dept, Tsinghua University, China \and School of
Software, Tsinghua University, China \and ECE Dept, Portland State
University, Portland, USA}

%
% NB: a more complex sample for affiliations and the mapping to the
% corresponding authors can be found in the file "llncs.dem"
% (search for the string "\mainmatter" where a contribution starts).
% "llncs.dem" accompanies the document class "llncs.cls".
%

\toctitle{Formal Specification and Verification of a Narrow
Bandwidth Protocol in PVS} \tocauthor{Hai Wan} \maketitle


\begin{abstract}
The paper presents a protocol for connection-establish service over
an extreme-narrow bandwidth channel. The protocol is modeled and
verified in a theorem proving system PVS. The PVS formalization and
proofs of properties are performed. The execution behaviors of the
protocol are modeled by state traces. Inductive methods were used to
verify three important properties of the protocol. The three
properties are held by the protocol for an arbitrary number of
agents. The effectiveness of the approach is demonstrated by
detection of a bug in the initial protocol implementation.
\keywords{Connection establishment protocol, Narrow bandwidth,
theorem proving, PVS}
\end{abstract}


\section{Introduction}

Protocol verification technologies have progressed in recent years.
A variety of tools are available for analyzing protocols. Due to the
complexity of protocols, it is of paramount importance that protocol
implementations be verified towards reliable systems. Communication
protocols are usually modeled by a set of finite-state machines that
generate the interaction between processes. Protocol verification is
a procedure to validate the logical correctness of these interaction
sequences and to detect potential design errors.

Model checking \cite{ec7} is employed for verifying a protocol. A
model checker works on a finite-state model of the system to be
verified, and a logical specification of a desired behavior of the
system model. It checks that the model adheres to the specification
by effectively searching the entire state space of the model. On the
other hand, theorem proving is envisioned as the most general
approach to verification. With theorem proving approaches, the
correctness condition of system is formalized as a theorem in a
mathematical logic and a mechanically checked proof of theorems is
generated using a general-purpose theorem proving system. The
approach has attained significant successes in verifying digital
system designs \cite{jh2}-\cite{ba6}. Theorem systems use powerful
formalisms such as higher-order logic that allow the verification
problem to be stated at many levels of abstraction.

In our system, connection establishment is of great importance,
since major applications are available only after a connection is
set up. Due to the limitations of the transfer channel, the
connection-establish protocol should be enough, i.e., the steps
token and bandwidth cost should be small. Classical
connection-establish protocols such as three-way handshake
\cite{sca9} can not fit our requirements very well. In this paper,
we present and verify a connection-establish protocol in PVS. We
proved the protocol holds the properties.

Three-way handshake protocol had been studied in \cite{ds1}. Our
approach differs from theirs in several aspects: protocols being
verified are different, transfer channels that the protocol based
on, the modeling of timeout and our approach consider arbitrary
pairs of participants.

PVS \cite{pvs8} is a mechanized environment for formal specification
and verification. PVS consists of an input language, a type checker,
and an interactive prover. The specification language of PVS is
based on the classical typed higher-order logic. With the expressive
language, the protocol can be translated into the PVS codes, and the
properties need to prove can be written as theorems. The powerful
primitive inference procedures provided by PVS can be used to reduce
the proof effort significantly.

The rest of the paper is organized as follows. In Section 2, a
detailed description about the system is given. Section 3 presents
the protocol and the properties must be hold. We show how we modeled
the protocol and proved the properties using PVS in Sections 4 and
5, respectively. Section 6 concludes the paper.
%

\section{The Narrow Bandwidth Protocol}
We describe the system and the protocols. The architecture of the
system we consider is shown in Fig 1. The system is composed of a
transfer channel and a network of agents. The transfer channel
provides a fundamental and very low level message deliver service
(MDS for short in the sequel). Every agent connecting to the channel
can use MDS to communicate with any other agent by exchanging
messages. Because of the underlying hardware on which MDS is
implemented, MDS has the following limitations and characteristics:

\begin{enumerate}
\item The bandwidth of MDS is very limited, i.e. the typical bandwidth
of the channel is about fifty bytes per ten seconds. In other words,
one agent can only send fifty bytes at one time, and the time span
between every two adjacent send-actions of one agent must be longer
than 10 seconds.
\item MDS is not reliable. It may lose messages when transferring.
\item Message delivery may delay, i.e., assuming that agent1
sends a message M to agent2 and agent2 receives M, then agent2 must
receive M within a time bound.
\item One agent can send at most one message at one time.
\item The order of received messages is correspond
with the order of messages sent, i.e. if an agent receives message
M1 before M2, then message M1 must be sent prior to M2. MDS is
similar to the cell phone's short messages service.
\end{enumerate}
\begin{figure}
\begin{center}
    \includegraphics[width=0.7\textwidth]{f1.eps}
    \caption {The architecture of the system}
\end{center}
\end{figure}
In our system, agents need to exchange long length content such as
files and long messages (longer than fifty bytes). MDS cannot
provide such service directly because of its limitations. In order
to solve this problem, we established a protocol stack which
consists of two layers: extreme-narrow-bandwidth-connection protocol
(ENBCP) and long-message-send protocol (LMSP). ENBCP is used to
establish and terminate a connection between two agents. After ENBCP
establishes a connection between two agents, which means they can
communicate with each other through an exclusive channel, any one of
the two can transfer long length content using LMSP. When finishing
transferring, agents can use ENBCP to terminate the connection. The
relation between ENBCP and LMSP is demonstrated in Fig 2.
\begin{figure}
\begin{center}
    \includegraphics[width=0.6\textwidth]{f2.eps}
    \caption {ENBCP and LMSP}
\end{center}
\end{figure}
There are a number of P to P transfer protocols that can be used as
LMSP with a few modifications. We do not discuss the modeling and
verification of these protocols in this paper. MDS requires that
ENBCP be as simple as possible. In other words, ENBCP should take as
less steps as possible, while the message length of each step should
be as short as possible. Protocols, such as three-way handshake of
TCP/IP, are not suitable for this situation. It takes long time to
establish a connection and the length of one frame of TCP/IP might
exceed the fifty bytes' limitation of MDS. ENBCP should be reliable,
since it is the basis of LMSP. We developed an ENBCP, which takes
four steps to establish and terminate a connection. In each step,
only 4 bits are used by ENBCP for identifying the message kind and
the rest bits can be used for storing the initialization data of
LMSP, etc.

In ENBCP, the agent which establishes a connection is called sender
and the other part of the connection is called receiver. An agent
can take only one role (sender or receiver) at a time. A agent has
five states: \emph{Idle}, \emph{BeforeSend}, \emph{Sending},
\emph{BeforeSendEnd} and \emph{Recving}. A sender agent has four
states: \emph{Idle}, \emph{BeforeSend}, \emph{Sending} and
\emph{BeforeSendEnd}. A receiver agent has two states: \emph{Idle}
and \emph{Recving}. There are four types of messages in ENBCP:
\emph{SendReq}, \emph{SendRes}, \emph{SendEndReq} and
\emph{SendEndRes}.

The pseudo-codes of ENBCP are shown in Fig 3. \emph{MQ} is a message
queue, whose items are of the form (\emph{from}, \emph{type}). If
MDS receives a message, it will automatically add an item to
\emph{MQ}. The field \emph{from} is the id of the agent that sent
the message, while the field \emph{type} is the message's type.
Given a message \emph{M}, we can access the field from by
\emph{M.from}. \emph{DQ} is a demand queue whose items are added by
the agent. Items of \emph{DQ} are of the form (\emph{with},
\emph{type}). The field \emph{with} is the id of the agent with whom
it wants to establish a connection. There are two types of demands:
\emph{EstablishConnection} and \emph{TerminateConnection}. For
example, if an agent wants to establish a connection with agent
\emph{B}, it adds an item (\emph{B}, \emph{EstablishConnection}) to
its \emph{DQ}. Variable state denotes for the agent's state and
variable \emph{cw} denotes for the agent with whom it wants to
establish a connection or already has established a connection.
Function \emph{Send(a, t)} denotes for sending a message of type
\emph{t} to agent \emph{a}.

\begin{figure}
\begin{center}
    \includegraphics[width=0.9\textwidth]{f3.eps}
    \caption {The pseudo-code of ENBCP}
\end{center}
\end{figure}

ENBCP consists of three parts:

\begin{enumerate}
\item  State transition in terms of the messages received.

If an agent receives a \emph{SendReq} and its state is \emph{Idle},
then it changes its state to \emph{Recving} and send a response
message \emph{SendRes}.

\item  State transition according to the demands.

After picking a \emph{EstablishConnection} demand from DQ and
verifying the condition (state = \emph{Idle} and no \emph{SendReq}
message in MQ), the agent sends a \emph{SendReq} message and sets
its \emph{cw} accordingly.

\item Timeout testing.

In ENBCP, an agent cannot stay at any \emph{non-Idle} state for an
arbitrary time. There are timeout thresholds for every
\emph{non-Idle} state. If an agent stays at \emph{Recving} state for
a time longer than \emph{time\_out\_Recving}, then it changes its
state back to \emph{Idle}.

\end{enumerate}

The state transition graph of the agent is shown in Fig 4. Messages
sent by the agent are marked with a "!" symbol. Messages received by
the agent are marked with a "?" symbol. The solid and dashed arrows
denotes for the state transitions result in message send/receiving
actions or timeout respectively.

\begin{figure}
\begin{center}
    \includegraphics[width=0.8\textwidth]{f4.eps}
    \caption {The state transition graph}
\end{center}
\end{figure}

A typical execution of the protocol is shown in Fig 5. The states of
the agent are marked above the lines and the messages of send and
receive are labeled by the arrows. It needs only two messages for
establishing and terminating a connection. The execution steps are:
1) if $agent_{1}$ wants to establish a connection with $agent_{2}$,
first it makes sure its state is \emph{Idle} and does not receive
any \emph{SendReq} in \emph{MQ}, then it sends \emph{SendReq} to
$agent_{2}$; 2) if $agent_{2}$ receives \emph{SendReq} and its state
is \emph{Idle}, then it sends \emph{SendRes} to $agent_{1}$; 3)
after $agent_{1}$ receives \emph{SendRes} from $agent_{2}$, which
means it has establish a connection with $agent_{2}$, it can start
LMSP with $agent_{2}$; 4) after executing LMSP, $agent_{1}$ sends
\emph{SendEndReq} to $agent_{2}$; 5) if $agent_{2}$ receives
\emph{SendEndReq} from $agent_{1}$, then it sends \emph{SendEndRes}
to $agent_{1}$; 6) $agent_{1}$ receives \emph{SendEndRes} from
$agent_{2}$, which means the connection is terminated.

\begin{figure}
\begin{center}
    \includegraphics[width=0.9\textwidth]{f5.eps}
    \caption {A typical execution of ENBCP}
\end{center}
\end{figure}

There are several properties that ENBCP should hold to guarantee the
correctness.

\textbf{Property 1.} If an agent \emph{A}'s state is \emph{Sending},
then there must be another agent \emph{B}, while \emph{B}'s state is
\emph{Recving}, \emph{B}'s id is equal to \emph{A}'s \emph{cw} and
\emph{B}'s \emph{cw} is equal to \emph{A}'s Id.

An agent \emph{A} is said to be at \emph{Ready} mode with agent
\emph{B} if and only if the following conditions hold: 1) \emph{A}'s
state is \emph{Sending}; 2) \emph{A}'\emph{cw} is \emph{B}'s
\emph{Id}; 3) \emph{B}'s state is \emph{Recving}; 4) \emph{B}'s
\emph{cw} is \emph{A}'s \emph{Id}.

It's obvious that when an agent is at \emph{Ready} mode with some
other agent, it can start the LMSP protocol safely. The first two
conditions are easily verified, since it only refers to local
variables. From property 1 we can infer that the first two
conditions imply the last two conditions. So the \emph{Ready} mode
check can be checked locally.

\textbf{Property 2.} At any time, two different agents are not
allowed to be at the Ready mode with the same agent. In other words,
if agent \emph{A} is at \emph{Ready} mode with agent \emph{C} and
agent \emph{B} is at \emph{Ready} mode with agent \emph{B}, then
\emph{A} is equal to \emph{B}.

\textbf{Property 3.} Any agent whose state is non-\emph{Idle} will
eventually reach \emph{Idle} state. This property expresses the
deadlock-free of ENBCP.

\section{ Modeling Protocol Primitives}

We elaborate on three theories to model the protocol. Theory
\emph{rt} contains the fundamental primitives about time, theory
\emph{env} specifies the model of the transfer channel and theory
\emph{protocol} defines the model of the protocol.

\subsection{Formalizing Time}

We define a theory \emph{rt} for time. We model time as type
\emph{int} in PVS. Based on Type \emph{Interval}, variant time
intervals are defined, such as \emph{co} represents left-closed and
right-open intervals, etc. Predicate \emph{during} is defined as a
moment in an interval and predicate \emph{before} as a moment before
the other.

\begin{verbatim}
    Time        : TYPE = int
    PTime       : TYPE = {t:Time|t>0}
    Interval        : TYPE = pred[Time]
    t,t0,t1         : VAR Time
    cc(t0,t1)       : Interval = {t|t0<=t AND t<=t1}
    co(t0,t1)       : Interval = {t|t0<=t AND t<t1}
    oc(t0,t1)       : Interval = {t|t0<t AND t<=t1}
    oo(t0,t1)       : Interval = {t|t0<t AND t<t1}
    during(t, I)        : bool = I(t)
    before(t0, t1)  : bool = t0 < t1
\end{verbatim}

\subsection{Formalizing Message Deliver Services}

Enumerative types \emph{StatusType} and \emph{MsgType} are used to
represent the states of an agent and the types of messages
respectively. \emph{Msg} which is a record type has one field:
\emph{MsgType}. The constant \emph{NoUser} denotes for \emph{None}
in ENBCP. All other agents are represented by the type \emph{User}.
The agents in the protocol are of type \emph{AnyUser} in the model.

\begin{verbatim}
    MsgType : TYPE = { SendReq, SendRes, SendDataReq,
        SendDataRes, SendEndReq, SendEndRes}
    StatusType : TYPE = { Idle, BeforeSend, Sending, Recving,
    BeforeSendEnd}
    Msg : TYPE = [#mtype : MsgType #]
    AnyUser : TYPE+ % = [# stype : StatusType #]
    NoUser : AnyUser
    User : TYPE+ = {u:AnyUser|u /= NoUser}
\end{verbatim}

The channel transfer delay and four time out thresholds are list
below. We should mention that the assumptions on these constants
such as $t\_timeout > 2*sr\_delay$ are necessary for proving the
first and second properties.

\begin{verbatim}
    sr_delay : PTime            % transfer delay
    send_interval : PTime           % interval between
                                    %two send actions
    t_timeout : {t:PTime|t>2*sr_delay}
                % time_out_BeforeSend and time_out_BeforeSendEnd
    t_windowtimeout_sender : {t:PTime|t>2*t_timeout}
                % time_out_Sending
    t_windowtimeout_receiver :
                {t:PTime |t>t_windowtimeout_sender+t_timeout}
                % time_out_Recving
\end{verbatim}

The \emph{send} and \emph{receive} actions are modeled by two
functions \emph{Send} and \emph{Recv} respectively. Predicate
\emph{Send(u1,m,t,u2)} specifies the fact that user \emph{u1} sends
a message \emph{m} to user \emph{u2} at time \emph{t}.
\emph{Recv(u1,m,t,u2)} means that user \emph{u1} receives a message
\emph{m} from user \emph{u2} at time \emph{t}.

\begin{verbatim}
    Send, Recv : [User, Msg, Time, User -> bool]
\end{verbatim}

We devise a list of axioms as constraints for the \emph{send} and
\emph{receive} actions to model characteristics of MDS.

\begin{verbatim}
OneUserCanSendOnlyOneMsgAtOneTime : AXIOM
    FORALL (u,u1,u2,m1,m2,t) :
        Send(u,m1,t,u1) AND Send(u,m2,t,u2)
            IMPLIES (m1 = m2) AND (u1 = u2)
RecvOrder0 : AXIOM
    Send(u1,m1,t1,u2) AND Send(u3,m2,t2,u4) AND
        before(t1, t2)AND Recv(u2,m1,t3,u1) AND
        Recv(u4,m2,t4,u3) IMPLIES before(t3, t4)
SendInterval : AXIOM
    Send(u,m1,t1,u1) AND Send(u,m2,t2,u2) AND before(t1, t2)
    IMPLIES before(t1, t2 - send_interval)
RecvBySend : AXIOM
    Recv(u1,m,t2,u2) IMPLIES
       EXISTS (t1) : (Send(u2,m,t1,u1) AND
       during(t2, oc(t1, t1 + sr_delay)))
OneMsgCanBeSendOnce : AXIOM
    FORALL (u1,u2,u3,u4,m,t1,t2) :
        Send(u1,m,t1,u2) AND Send(u3,m,t2,u4)
        IMPLIES (u1 = u3) AND (t1 = t2) AND (u2 = u4)
MsgCanBeRecvOnce : AXIOM
    Recv(u2,m,t1,u1) AND Recv(u4,m,t2,u3)
    IMPLIES (u1 = u4) AND (t1 = t2) AND (u1 = u3)
\end{verbatim}

Axiom \emph{OneUserCanSendOnlyOneMsgAtOneTime} implies that one user
can send only one message at one time. Axiom \emph{RecvOrder0}
describes the message-ordering characteristic of MDS (the fifth
characteristic of MDS in section 2). Axiom \emph{SendInterval}
describes the fact that the time span between two adjacent
send-actions of one agent must be longer than the constant
\emph{send\_interval}. Axiom \emph{RecvBySend} means that if user
\emph{u1} receives a message \emph{m} from user \emph{u2} at time
\emph{t2}, there must be a time \emph{t1}, on which \emph{u2} sent
the message \emph{m}. And \emph{t1} and \emph{t2} satisfy the
deliver delay constraint. The last two axioms are auxiliary.

\section{Formalizing the Narrow Bandwidth Protocol in PVS}

We model the connection protocol in the theory \emph{protocol}. The
status of an agent is modeled by a record type \emph{OneStatus} of
two fields \emph{StatusType} and \emph{User}. \emph{cw} of type
\emph{User} denotes the user with which the agent is communicating.

\begin{verbatim}
    OneStatus : TYPE = [# st : StatusType, cw : User #]
\end{verbatim}

Type \emph{OneUserTrace} denotes for the status at a certain point
of time. Every item in \emph{OneUserTrace} is a status trace with
respect to time. Given an item \emph{out} of type
\emph{OneUserTrace} and a time \emph{t}, \emph{out(t)} denotes for
the status at time t. Any element in type \emph{Traces} is a
function maps from \emph{User} to \emph{OneUserTrace}. Given an item
\emph{T} of type \emph{Traces}, a \emph{User} \emph{u} and a time
\emph{t}, \emph{T(u)(t)} denotes for the \emph{status} of agent
\emph{u} at time \emph{t}.

\begin{verbatim}
    OneUserTrace : TYPE = [Time -> OneStatus]
    Traces : TYPE = [User -> OneUserTrace]
\end{verbatim}

Since the elements of \emph{Traces} are arbitrary and we don't put
any constraints on them, it is possible that, given a \emph{T} of
\emph{Traces}, a \emph{u} of \emph{User} and a \emph{t} of
\emph{time} that \emph{\emph{T(u)(t)}.StatusType = Sending} and
\emph{T(u)(t+1).StatusType = Recving}, which obviously disobeys the
ENBCP. In order to avoid this violation, we devise sorts of
constraints (predicates) about \emph{Traces} based on ENBCP. There
are five sorts of predicates.

\subsection{ Formalizing State Transitions}

This type of predicate describes the valid changes between states.
Take predicate \emph{VSC\_Idle} for example; it denotes that after
state \emph{Idle}, the valid states next time are \emph{Idle},
\emph{BeforeSend} or \emph{Recving}. The predicates about
\emph{BeforeSend}, \emph{Sending}, \emph{Recving} and
\emph{BeforeSendEnd} are of the same form.

\begin{verbatim}
VSC_Idle(outr) : bool =
        FORALL (t) : (outr(t)`st = Idle) IMPLIES
            (outr(t+1)`st = Idle) OR (outr(t+1)`st = BeforeSend) OR
            (outr(t+1)`st = Recving)

\end{verbatim}

\subsection{Formalizing Timeout}

When the time span one user stays at any non-\emph{Idle} state
exceeds the timeout threshold, the state will change to \emph{Idle}
next time. For instance, if one agent stays at state
\emph{BeforeSend} for a time span equal to \emph{t\_timeout}, its
state will change to \emph{Idle} or \emph{Sending}.

\begin{verbatim}
VSC_BeforeSendTimeout(outr) : bool =
    FORALL (t1) :BeingStatus(outr,t1-t_timeout+1,t1,BeforeSend)
        IMPLIES
            outr(t1+1)`st = Sending OR outr(t1+1)`st = Idle
\end{verbatim}

\subsection{Formalizing the Communicating Counterpart}
In the protocol, each user has variable \emph{cw} to record the user
with whom he communicates. The following predicates represent the
constraints on the valid change of \emph{cw} are given in the model.

\begin{verbatim}
VSWC_Idle(outr) : bool =
    FORALL (t) : (outr(t)`st = Idle) IMPLIES (outr(t)`cw = NoUser)
VSWC_ChangeWith(outr) : bool =
    FORALL (t) :
        (outr(t+1)`cw /= outr(t)`cw) IMPLIES (outr(t+1)`st /= outr(t)`st)
VCWC_IdleToBeforeSend(outr) : bool = FORALL (t) : (outr(t)`st =
Idle) AND (outr(t+1)`st = BeforeSend)
        IMPLIES
            outr(t+1)`cw /= NoUser
VCWC_BeforeSendToSending(outr) : bool =
    FORALL (t) : (outr(t)`st = BeforeSend) AND (outr(t+1)`st = Sending)
        IMPLIES
            outr(t)`cw = outr(t+1)`cw
VCWC_SendingToBeforeSendEnd(outr) : bool =
    FORALL (t) : (outr(t)`st = Sending) AND (outr(t+1)`st = BeforeSendEnd)
        IMPLIES
            outr(t)`cw = outr(t+1)`cw
VCWC_IdleToRecving(outr) : bool =
    FORALL (t) : (outr(t)`st = Idle) AND (outr(t+1)`st = Recving)
        IMPLIES
            outr(t+1)`cw /= NoUser
\end{verbatim}

\subsection{Formalizing Transfer Events}
Every send action has its conditions and effects. For instance, when
a send \emph{SendReq} action takes place at time \emph{t}, we can
infer that the agent's state is \emph{Idle} and it doesn't receive
\emph{SendReq} at time \emph{t} and the agent's state is
\emph{BeforeSend} at \emph{time (t+1)}. We use condition and effect
to specify send actions.

\begin{verbatim}
VA_Send_SendReq(u,tr) : bool =
        FORALL (t,u1,m) :
            Send(u,m,t,u1) AND (m`mtype = SendReq)
            IMPLIES
(tr(u)(t)`st = Idle) AND (NOT EXISTS (u2) : (Recv(u,m,t,u2) AND
(m`mtype = SendReq))) AND (tr(u)(t+1)`st = BeforeSend) AND
(tr(u)(t+1)`cw = u1)
\end{verbatim}

In the above specification, $"(tr(u)(t)`st = Idle) AND (NOT EXISTS
(u2) : (Recv(u,m,t,u2) AND (m`mtype = SendReq)))"$ is the condition
of the send action, and $"(tr(u)(t+1)`st = BeforeSend) AND
(tr(u)(t+1)`cw = u1)"$ is the effect of the action. The
specifications about \emph{SendEndReq}, \emph{SendRes} and
\emph{SendEndRes} are of the same form and are omitted here.

Based on the protocol, we infer that the state of an agent changes
if and only if one of the following conditions holds: 1)  The agent
stays at non-Idle state exceeds the timeout threshold 2)  The agent
sends a message 3)  The agent receives a message.

Predicate \emph{VSCC\_Idle\_BeforeSend} denotes that if agent
\emph{u}'s state changes from \emph{Idle} to \emph{BeforeSend} at
time \emph{t}, then \emph{u} must send a \emph{SendReq} message at
time \emph{t}.

\begin{verbatim}
VSCC_Idle_BeforeSend(u,tr) : bool =
        FORALL (t) :
            (tr(u)(t)`st = Idle) AND (tr(u)(t+1)`st = BeforeSend)
            IMPLIES
            (EXISTS (u1,m) : Send(u,m,t,u1) AND m`mtype = SendReq)
\end{verbatim}

Predicate \emph{VSCC\_Recving\_Idle} denotes that if agent
\emph{u}'s state changes from \emph{Recving} to \emph{Idle} at time
\emph{t}, then \emph{u} must receive a \emph{SendEndReq} message at
time \emph{t} from agent \emph{cw} or \emph{u} has been at
\emph{Recving} state for a time span longer than the timeout
threshold.

\begin{verbatim}
VSCC_Recving_Idle(u,tr) : bool =
    FORALL (t) :
            (tr(u)(t)`st = Recving) AND (tr(u)(t+1)`st = Idle)
        IMPLIES
            ((EXISTS (u1,m) : Recv(u,m,t,u1) AND m`mtype = SendEndReq
            AND tr(u)(t)`cw = u1)
                OR
            BeingStatus(tr(u),t-t_windowtimeout_receiver+1,t,Recving))
\end{verbatim}

We have defined this kind of predicates for all the valid state
change (\emph{BeforeSend} to \emph{Sending}, \emph{Sending} to
\emph{Idle}, \emph{BeforeSend} to \emph{Idle}, \ldots).

\section{Mechanically Proved Properties}

We formalize the three properties described in Section 2 as follows.

\textbf{Property 1.} If an agent \emph{A}'s state is \emph{Sending},
then there must be another agent \emph{B} such that \emph{B}'s state
is \emph{Recving}, \emph{B}'s \emph{id} equals \emph{A}'s \emph{cw}
and \emph{B}'s \emph{cw} equals \emph{A}'s \emph{Id}.

\begin{verbatim}
FinalTheorem_1 : THEOREM
    ValidTrace(tr) IMPLIES FORALL (t,u1) :
    tr(u1)(t)`st = Sending IMPLIES EXISTS (u2) : tr(u1)(t)`cw = u2 AND
    tr(u2)(t)`st = Recving AND tr(u2)(t)`cw = u1
\end{verbatim}

\emph{ValidTrace(tr)} denotes that \emph{tr} is a trace satisfying
all the five sorts of predicates described in section 3. Theorem
\emph{FinalTheorem\_1} shows that if an agent \emph{u1} is at
\emph{Sending} state at time \emph{t}, then at time \emph{t} there
must exist an agent \emph{u2}, whose state is \emph{Recving} and
with which \emph{u1} establish connection to.

\textbf{Property 2.} At any time, two different agents are not
allowed to be at the \emph{Ready} mode with the same agent. In other
words, if agent \emph{A} is at \emph{Ready} mode with agent \emph{C}
and agent \emph{B} is at \emph{Ready} mode with agent \emph{B}, then
\emph{A} is equal to \emph{B}.

\begin{verbatim}
FinalTheorem_2 : THEOREM ValidTrace(tr)
    IMPLIES FORALL (t,u1,u2,u3):
        tr(u1)(t)`st = Sending AND tr(u2)(t)`st = Sending AND
        tr(u1)(t)`cw = u3 AND tr(u2)(t)`cw = u3
        IMPLIES u1 = u2
\end{verbatim}

Theorem \emph{FinalTheorem\_2} shows that, if two agents both are at
Sending state and communicate with the same agent, then the two
users must be equal.

\textbf{Property 3.} Any agent with state non-\emph{Idle} will
eventually reach \emph{Idle} state. This property expresses the
deadlock-freeness of ENBCP.

\begin{verbatim}
FinalTheorem_3 : THEOREM ValidTrace(tr)
    IMPLIES FORALL (t,u) : tr(u)(t)`st /= Idle
        IMPLIES
        EXISTS (t1) : before(t, t1) AND tr(u)(t1)`st = Idle
\end{verbatim}

The theorem \emph{FinalTheorem\_3} is straightforward. To prove the
first two theorems, we need prove the following theorem.

\begin{verbatim}
BeforeSendingExist : THEOREM ValidTrace(tr)
    IMPLIES FORALL (t) :
    tr(u)(t)`st = Sending IMPLIES EXISTS (t0,m1,m2,u1,t1,t2) : t2 < t
    AND BeingStatus(tr(u),t2+1,t,Sending) AND tr(u)(t2)`st = BeforeSend
    AND  t0 <= t2 AND BeingStatus(tr(u),t0,t2,BeforeSend) AND
    tr(u)(t0-1)`st = Idle AND t0<=t1 AND t1<=t2 AND Send(u1,m2,t1,u) AND
    m2`mtype = SendRes AND Recv(u,m2,t2,u1) AND u1 = tr(u)(t)`cw AND
    Send(u,m1,t0-1,u1) AND m1`mtype = SendReq AND Recv(u1,m1,t1,u) AND
    (t - t0 <= t_timeout + t_windowtimeout_sender) AND
    BeingStatus(tr(u1),t1+1,t,Recving)
\end{verbatim}

The theorem can be illustrated in Fig 6. Given a user \emph{u1} and
a time \emph{t}, if \emph{u1}'s state is \emph{Sending} at \emph{t},
then we can infer the following conclusions:

\begin{enumerate}
\item There exists three times \emph{t0}, \emph{t1}, \emph{t2} and a
user \emph{u2};
\item \emph{u1}'s state is \emph{Idle} at time \emph{t0},
\emph{u1}'s state is \emph{BeforeSend} between $t0+1$ and \emph{t2},
\emph{u1}'s state is \emph{Sending} between $t2+1$ and \emph{t};
\item \emph{u2}'s \emph{cw} is \emph{u1} and \emph{u1}'s \emph{cw} is
\emph{u2} at time \emph{t};
\item \emph{u1} sends a \emph{SendReq}
to \emph{u2} at \emph{t0}, \emph{u2} receives the request at
\emph{t1} and sends a \emph{SendRes} to \emph{u1} at \emph{t1}, and
\emph{u1} receives the response at \emph{t2};
\item \emph{u2}'s
state is \emph{Recving} between $t1+1$ and \emph{t};
\item Time span
from \emph{t0} to \emph{t} is no more than $t\_timeout +
t\_windowtimeout\_sender$.
\end{enumerate}

\begin{figure}
\begin{center}
    \includegraphics[width=0.7\textwidth]{f6.eps}
    \caption {The theorem BeforeSendingExist}
\end{center}
\end{figure}

To show theorem \emph{BeforeSendingExist}, we need to prove 15
lemmas. The proof process is tedious and lengthy, we omit them here.
Theorem \emph{FinalTheorem\_1} can be implied directly from the
theorem \emph{BeforeSendingExist}. To prove theorem
\emph{FinalTheorem\_3}, we need to prove the following four lemmas
based on the timeout mechanism of ENBCP.

\begin{itemize}
\item \textbf{Lemma 1.} If an agent's state is \emph{Recving}, it will eventually
reach \emph{Idle}.
\item \textbf{Lemma 2.} If an agent's state is
\emph{BeforeSendEnd}, it will eventually reach \emph{Idle}.
\item \textbf{Lemma 3.} If an agent's state is \emph{Sending}, it will
eventually reach \emph{Idle} or \emph{BeforeSendEnd}.
\item \textbf{Lemma 4.} If an agent's state is \emph{BeforeSend}, it will eventually reach \emph{Idle} or
\emph{Sending}.
\end{itemize}

For property 2, from theorem \emph{BeforeSendingExist}, we know that
there must be two moments: \emph{t1} and \emph{t2}, as shown in Fig
7. There are three relations between \emph{t1} and \emph{t2}: $t1 >
t2$, $t1 < t2$ and $t1 = t2$. Under the condition of $t1 = t2$, we
can prove that $u1 = u2$, since one agent can send only one message
at a time (\emph{u3} at time \emph{t1}). In case $t1 < t2$, from
\emph{BeforeSendingExist} we can infer that \emph{u3}'s state must
be \emph{Recving} (for \emph{u1}) and \emph{Idle} (for \emph{u2}),
which causes a contradiction. The case $t1 > t2$ is similar.

\begin{figure}
\begin{center}
    \includegraphics[width=0.65\textwidth]{f7.eps}
    \caption { Proof of FinalTheorem\_2}
\end{center}
\end{figure}

Our proof detected a bug of the initial ENBCP protocol design. In
the initial version of ENBCP, the constant
\emph{t\_windowtimeout\_receiver} is assumed to be larger than the
constant \emph{t\_windowtimeout\_sender}. During the proof process
we found this assumption is too weak to prove the theorem
\emph{\emph{BeforeSendingExist}}. After carefully study on the sub
goals that cannot be proved, we strengthened this assumption to
$t\_windowtimeout\_receiver > t\_windowtimeou\_sender + t\_timeout$,
then everything was done.

The assumptions about the delay and timeout thresholds are necessary
for the correctness of the properties. But these assumptions are
qualitative; the efficiency of the protocol entails further
investigation. Timed-automata can be used to model and analyze the
protocol and the transfer channel.

\section{Conclusions}

In this paper we presented a protocol of establishing connections on
an extremely narrow bandwidth transfer channel. We modeled the
protocol in the theorem proving system PVS. The execution behaviors
of the protocol are modeled by state traces. The proof process
detected a bug of the initial protocol implementation. Inductive
methods were used to verify three important properties of the
protocol. The three properties are held by the protocol for an
arbitrary number of agents.

\begin{thebibliography}{4}

\bibitem{ds1}
Schwabe, D.: Formal specification and verification of a connection
establishment protocol. Proceedings of the seventh symposium on Data
communications, pp.11--26, October 27-29, Mexico City, Mexico (1981)

\bibitem{jh2}
Hooman, J.: Compositional Verification of a Distributed Real-Time
Arbitration Protocol. (1994)

\bibitem{vr3}
Rusu, V.: Verifying a Sliding Window Protocol using PVS. 21st
International Conference on Formal Techniques for Networked and
Distributed Systems, pp.251--268 (2001)

\bibitem{dv4}
Dang, V.H.: Modelling and Verification of Biphase Mark Protocols in
Duration Calculus Using PVS. Proceedings of the International
Conference on Applications of Concurrency to System Design (1998)

\bibitem{dc5}
Chkliaev, D., Stok, P.v.d., Hooman, J.: Formal Modeling and Analysis
of Atomic Commitment Protocols. Proceedings of the Seventh
International Conference on Parallel and Distributed Systems (2000)

\bibitem{ba6}
Akbarpour, B.,Tahar, S.: Error Analysis of Digital Filters using
Theorem Proving. In: K. Slind, A. Bunker and G. Gopalakrishnan
(Eds.), Theorem Proving in Higher Order Logics, Lecture Notes in
Computer Science 3223, Springer Verlag, pp. 1--16. (2004)

\bibitem{ec7}
Clarke, E., Grumberg, O., Peled, D.: Model Checking, MIT Press
(2000)

\bibitem{pvs8}
PVS specification and verification system,
http://pvs.csl.sri.com/index.shtml

\bibitem{sca9}
Sunshine,C.A., Dalal,Y.K.: Connection Management in Transport
Protocols. Computer Network 2, (6), December, (1978)

\end{thebibliography}

\end{document}
